$\forall$$f$, $g$:$x$:Knd fp$\rightarrow$ Type, $x$:Knd. ($\uparrow$$x$ $\in$ dom($f$ $\oplus$ $g$)) $\Leftarrow\!\Rightarrow$ (($\uparrow$$x$ $\in$ dom($f$)) $\vee$ ($\uparrow$$x$ $\in$ dom($g$)))